es:ES, A, V:Type, i:Id, knd:Knd, ds:x:Id fp Type, f:(State(ds)V(A + Top)).
(e:E. (loc(e) = i)  (kind(e) = knd)  ((valtype(e) r V) & (state@loc(e) r State(ds))))
 (e:E.
 ((e  es-trigger(es;i;knd;ds;f)))
  (loc(e) = i & kind(e) = knd & (isl(f((state when e),val(e)))))) 

latex

Definitions

b, can-apply(f;x), e  X, es-trigger(es;i;knd;ds;f), ES, t  T, Type, Id, Knd, x. t(x), x:A. B(x), a:A fp B(a), Top, left + right, x:AB(x), State(ds), state@i, valtype(e), x:A  B(x), P & Q, kind(e), s = t, P  Q, loc(e), E, val(e), P  Q, (state when e), isl(x), , ff, <a, b>, f(a), , P  Q, P  Q, A, True, b, p q, T, Unit, a = b, a = b, p  q, Atom$n, t.1, A c B, False, vartype(i;x), f(x)?z, IdDeq, x.A(x), @i discrete ds, {T}, SQType(T), tt, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , Void

Lemmas

false wf, btrue wf, bfalse wf, es-state-subtype2, es-state-subtype, fpf-cap wf, id-deq wf, es-state-subtype-iff, assert-eq-knd, eqtt to assert, assert of band, and functionality wrt iff, eqff to assert, squash wf, true wf, bnot thru band, assert of bor, or functionality wrt iff, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, bor wf, bnot wf, not wf, band wf, eq knd wf, eq id wf, bool wf, assert wf, isl wf, es-state-when wf, es-val wf, es-E wf, es-loc wf, es-kind wf, es-valtype wf, es-state wf, decl-state wf, top wf, fpf wf, Knd wf, Id wf, event system wf